Flow networks are inductively defined, assembled from small components to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. We carry out this induction formally using a domain-specific language (DSL). Associated with our DSL are a semantics and a typing theory. The latter gives rise to a system of formal annotations that enforce desirable properties of flow networks as invariants across their interfaces. A prerequisite for a typing theory is a formal semantics, i.e., a rigorous characterization of flows that are safe (or just feasible in this report) for the network, possibly restricted to satisfy additional efficiency or safety requirements. We give a detailed presentation of a denotational semantics only, but also point out the elements that an equivalent operational semantics must include.
展开▼
